(set-logic QF_UF)
(declare-sort U 0)
(declare-fun a1 () U)
(declare-fun b1 () U)
(declare-fun c1 () U)
(declare-fun a2 () U)
(declare-fun b2 () U)
(declare-fun c2 () U)
(declare-fun start () U)
(declare-fun f (U) U)
(declare-fun g (U) U)
(declare-fun h (U U) U)
(declare-fun h2 (U U U) U)
(assert (and
  (= a1 (f b1))
  (= b1 (h c1 c2))
  (= c1 (f a1))
  (= a2 (g b2))
  (= b2 (g c2))
  (= c2 (h2 a1 b1 a2))
  (= start (h b1 a2))
))
(check-sat)
